Definitions | n+m, fib(n), , s = t, #$n, n - m, , a < b, P ![](../FONT/eq.png) Q, A B, x:A. B(x), {x:A| B(x)} , t T, x:A![](../FONT/dash.png) B(x), i j , Void, False, A, -n, , callbyvalue(a;x.B(x)), has-value(a), f(a), True, T, {T}, SQType(T), s ~ t, left + right, P Q, Dec(P), (i = j), P & Q, b, ![](../FONT/not.png) b, x:A B(x), Type, p ![](../FONT/and.png) q, , p ![](../FONT/or.png) q, P ![](../FONT/if_big.png) Q, P ![](../FONT/if_big.png) ![](../FONT/eq.png) Q, Unit, x.A(x) |